#include <PDTSMT2Visitor.h>

#include <PDTNumVar.h>
bool
PDTNumVar::
SMT2visit(PDTSMT2Visitor & vis) {
    vis.ss << " (declare-fun " << getName() << " () Var)" << endl;
    return true;
}

#include <PDTAssign.h>
bool
PDTAssign::
SMT2visit(PDTSMT2Visitor & vis) {

#if 0
    
x=5;
(declare-fun s1 () Statement)
(assert (= (s02i s1) 5))
(assert (inGamma0 x s1))
(assert (not (inGamma0 y s1))) or 

(assert (forall (v Var) (=> (not (= v x)) (not (inGamma0 v s1)))))
#endif
    vis.ss << " (declare-fun " ;
    //TODO: FIX THIS vis.ss << getName() ;
        vis.ss << " () Var)" << endl;
    return true;
}
